% Chapter 1

\chapter{Propriet\u a\c tile System F\^{}}
\label{Capitolul4}

% 10 pag
\section{Siguran\c ta}
\begin{remark}
\^ In aceast\u a sec\c tiune toate tipurile folosite, vor fi tipuri cu dimensiune. Pentru simplitate, atunci c\^ and nu este pericol de confuzie \^ intre tipurile System \frec \c si tipurile cu dimensiune, voi scrie $\sigma$ \^ in loc de $\overline{\sigma}$.
\end{remark}
\begin{proposition}
System \fhat are proprietatea de progres.
\end{proposition}
\begin{proof}[Demonstra\c tie]
Vom considera o expresie $e$ \^ in System \fhat astfel \^ inc\^ at $\exists \sigma,\Gamma.\: \Gamma \vdash e : \sigma$. \^ In func\c tie de structura lui $e$ avem mai multe cazuri.
\begin{enumerate*}
  \item ${\bf e = e_1\app e_2} $. Cum $e$ este validat\u a de sistemul de tipuri, \^ inseamna c\u a $\exists \sigma , \tau.\,e_1 : \sigma \to \tau$. \^ In cazul \^ in care $e_1$ nu este valoare, $\exists e_1'. e_1 \to e_1'$ si deci $e \to e_1'\app e_2$ propozi\c tia este demonstrat\u a. Altfel $e_1$ poate fi:
        \begin{enumerate*}
            \item Func\c tie lambda $\lambda x : |\sigma|.e_1'$ caz in care $e \to [x \mapsto e_2] e_1'$
            \item Func\c tie textual recursiv\u a $(\text{letrec}_{d\app|\tau|\to|\sigma|} f := g)$, caz \^ in care
                $$e \to [f \mapsto (\text{letrec}_{d\app|\tau|\to|\sigma|} f := g)]g \app e_2 $$
        \end{enumerate*}
  \item ${\bf e = e_1\app [|{\sigma}|]}$ . Daca $e_1$ este valoare, atunci singura form\u a pe care poate s\u a o aib\u a este  $\Lambda X.e_1'$ \c si deci $e\to [X \mapsto {\sigma}]e_1'$. Dac\u a $e_1$ nu este valoare, propozi\c tia se demonstreaz\u a analog cu cazul anterior.
  \item ${\bf e = \text{case}_{|\sigma|}\ e' \text{ of } \{ \vec{c} \Rightarrow \vec{e} \} }$. Din regula {\scriptsize (T-CASE)} avem c\u a $e': d\app \tau$. Deci singura valoare posibil\u a pentru $e'$ este de forma $c_k\app \tau\app t_1\app t_2\app \dots\app t_n$ caz \^ in care se poate aplica regula de reducere {\scriptsize (E-CASE)}.\qedhere
\end{enumerate*}
\end{proof}
Vom da \^ int\^ ai demonstra\c tia propriet\u a\c tii de conservare folosind o serie de leme al caror enun\c t se gase\c ste la sf\^ ar\c situl demonstra\c tiei. Majoritatea dintre ele sunt leme care apar \^ in orice de\-mon\-stra\-\c ti\-e de conservare precum leme de inversiune a regulilor de tip sau lema de conservare la substitu\c tie. Aceasta demonstra\c tie extinde demonstra\c tia din \citep{967408} pentru tipuri polimorfice.
\begin{proposition}
System \fhat are proprietatea de conservare.
\end{proposition}

\begin{proof}[Demonstra\c tie]
Fie $e_1$ o expresie astfel \^ inc\^ at $\Gamma \vdash e_1 : \sigma $ \c si $e_1 \to e_2$. Trebuie s\u a demonstr\u am c\u a $\Gamma \vdash e_2:\sigma$. Vom demonstra prin induc\c tie structural\u a pe arborele de deduc\c tie al propozi\c tiei $\Gamma \vdash e_1 : \sigma $. \^ In func\c tie de ultima regul\u a de deduc\c tie aplicat\u a, avem mai multe cazuri, dintre care le voi trata doar pe cele interesante:
\begin{description}
  \item[{\scriptsize (T-CASE)}] Atunci $e_1 = \text{case}_{|\sigma|}\ e_1' \text{ of } \{ \vec{c}\Rightarrow \vec{e} \} \text{ si } \Gamma \vdash e_1' : d^{\hat{s}}\app\tau $ .
        \begin{enumerate*}
        \item Dac\u a ultima regul\u a de evaluare aplicat\u a \^in $e_1 \to e_2$ este regula {\scriptsize (CTX-CASE)}, atunci $\exists e_2'. e_1' \to e_2' \text{ si } e_2 = \text{case}_{\sigma}\ e_2' \text{ of } \{ \vec{c}\Rightarrow \vec{e} \}$. Din ipoteza de induc\c tie $\Gamma \vdash e_1' : d^{\hat{s}} \app \tau \Rightarrow \Gamma \vdash e_2': d^{\hat{s}}\app\tau$. Din lema \ref{inversion} pentru $\Gamma \vdash e_2 : \sigma $ \c si regula {\scriptsize (T-CASE)} avem ca $\Gamma \vdash e_2 : \sigma $.
        \item Dac\u a ultima regula de evaluare aplicat\u a este {\scriptsize (E-CASE)} atunci $e_1' = c_k\app[|\tau|]\app t$ si deci $e_2 = e_k \app t$. Pentru simplitate am considerat cazul \^ in care constructorul este unar. Conform regulii de tip {\scriptsize (T-CASE)} avem c\u a $\exists s$ astfel \^ inc\^ at:
                 \begin{equation}
                 \Gamma \vdash e'_1 : d^{\hat{s}} \tau \ \ \wedge \ \
                 \Gamma \vdash e_k : [X \mapsto \tau, \iota \mapsto s] \theta_k \to \sigma \ \ \wedge \ \
                 \Gamma \vdash c_k : \Pi X. \theta_k \to d^{\hat{\iota}}\app X
                 \end{equation}
            Acum aplic\u am lema \ref{inversion} pentru $\Gamma \vdash e_1' = c_k\app[|\tau|]\app t : d^{\hat{s}}\app\tau$ avem c\u a
            \begin{equation} \label{eq1}
            \exists \gamma,\sigma.
                \Gamma \vdash c_k\app [|\tau|] : \gamma \to \sigma  \quad \wedge \quad
                \Gamma \vdash t : \gamma \quad \wedge \quad
                \sigma \sqsubseteq d^{\hat{s}}\app \tau
            \end{equation}
            Aplic\^ and \^ inca odata lema \ref{inversion} pentru $\Gamma \vdash c_k\app [|\tau|] : \gamma \to \sigma$ ob\c tinem
            \begin{equation}\label{eq2}
                \Gamma \vdash c_k\app : \Pi X. \gamma' \quad \wedge \quad
                [X\mapsto \tau] \gamma' \sqsubseteq \gamma \to \sigma
            \end{equation}
            Aplic\^ and \^ inca odata lema \ref{inversion} pentru $\Gamma \vdash c_k\app : \Pi X. \gamma' $ ob\c tinem
            \begin{equation}  \label{eq3}
                \exists r.\gamma' \equiv \gamma'' \to \sigma'' \quad \wedge \quad
                \gamma'' \sqsubseteq [\iota \mapsto r] \theta_k \quad \wedge \quad
                d^{\hat{r}}\app X \sqsubseteq \sigma''
            \end{equation}
            Din rela\c tiile \eqref{eq2} \c si \eqref{eq3} \c si lema \ref{subst_sub} ob\c tinem
            \begin{equation} \label{eq4}
                [X \mapsto \tau] (\gamma'' \to \sigma'') \sqsubseteq \gamma \to \sigma \Rightarrow \gamma \sqsubseteq [X \mapsto \tau] \gamma'' \sqsubseteq [X \mapsto \tau][\iota \mapsto r] \theta_k
            \end{equation}
            Din rela\c tiile \eqref{eq1},\eqref{eq2} \c si \eqref{eq3} \c si lema \ref{stage_inversion} ob\c tinem
            \begin{equation} \label{eq5}
            \begin{split}
                [X \mapsto \tau] (\gamma'' \to \sigma'') \sqsubseteq \gamma \to \sigma
                    &\Rightarrow [X \mapsto \tau] d^{\hat{r}} X \sqsubseteq [X \mapsto \tau] \sigma'' \sqsubseteq \sigma \sqsubseteq d^{\hat{s}} \tau \\
                    &\Rightarrow d^{\hat{r}} \tau \sqsubseteq d^{\hat{s}} \tau\\
                    &\Rightarrow r \le s
            \end{split}
            \end{equation}
            Din \eqref{eq4} \c si \eqref{eq5}, lema \ref{stage_pos_subst} \c si din faptul c\u a tipul de date $d$ fiind inductiv, $d^{\iota}$ \c si deci $\iota$ apare \^ in $\theta_k$ pe pozi\c tii pozitive:
            \begin{equation}\label{eq6}
                \gamma \sqsubseteq [X \mapsto \tau, \iota \mapsto s] \theta_k
            \end{equation}
            Conform \eqref{eq6},\eqref{eq1} \c si {\scriptsize (T-APP)} : $\Gamma \vdash e_2 = e_k \app t : \sigma$.
        \end{enumerate*}
  \item[{\scriptsize (T-APP)}] Atunci $e_1 = t_1 \app t_2$ \c si $\Gamma \vdash t_1 : \tau_1 \to \tau_2 $, $\Gamma \vdash t_2 : \tau_1 $, $\Gamma \vdash e_1 : \tau_2 $.
        \begin{enumerate*}
        \item Dac\u a ultima regul\u a de evaluare aplicat\u a este {\scriptsize (CTX-APP)}, atunci propozi\c tia se demonstreaz\u a folosind ipoteza de induc\c tie ca \c si \^ in cazul anterior.
        \item Dac\u a ultima regul\u a de evaluare aplicat\u a este {\scriptsize (E-APP)}, atunci $t_1 = \lambda x : |\tau_1'| . e$ \c si deci $e_2 = [x \mapsto t_2] e$. Folosind lema \ref{inversion} pentru $\Gamma \vdash t_1 : \tau_1 \to \tau_2$ o\c btinem:
            \begin{equation}\label{eq7}
                \Gamma, x:\tau_1' \vdash e : \tau_2' \quad\wedge\quad \tau_1 \sqsubseteq \tau_1' \quad\wedge\quad \tau_2' \sqsubseteq \tau_2
            \end{equation}
            Din \eqref{eq7} conform regulii {\scriptsize (T-SUB)} avem c\u a $\Gamma \vdash t_2 : \tau_1'$. De aici, conform lemei de substitu\c tie \ref{subst_var} si \eqref{eq7} ob\c tinem:
            \begin{equation}
                \Gamma \vdash [x \mapsto t_2] e : \tau_2' \sqsubseteq \tau_2
            \end{equation}
        \item Dac\u a ultima regul\u a de evalure este  {\scriptsize (E-LETREC)}, avem $t_1 = (\text{letrec}_{d\app|\tau| \to |\sigma|}f := g)$ si $t_2 = c\app [|\tau|] \app e$ si deci $e_2 = ([f \mapsto (\text{letrec}_{d\app|\tau| \to |\sigma|}f := g)]g)\app(c\app [|\tau|] \app e)$. Aplic\^ and lema \ref{inversion} pentru $\Gamma \vdash t_1 : \tau_1 \to \tau_2$ ob\c tinem:
            \begin{gather}
                \label{eq8} \forall \iota. \:\Gamma,f : d^{{\iota}} \tau \to \sigma \vdash g : [\iota \mapsto \hat{\iota}] (d^{{\iota}}\app \tau \to \gamma) \\
                \label{eq9} \exists s. [\iota \mapsto s] (d^{{\iota}} \tau \to \sigma) \sqsubseteq \tau_1 \to \tau_2 \\
                \label{eq10} \iota \text{ {pos} } \sigma \text{ {si} } \iota \text{ {nu apare in} } \Gamma , \tau
            \end{gather}
            Din \eqref{eq9}, \eqref{eq10} \c si regula de subtip pentru func\c tii, avem $\tau_1 \sqsubseteq d^{s} \app \tau$ si $[\iota \mapsto s]\sigma \sqsubseteq \tau_2$ \c si folosind  lema \ref{sub_inversion}
            \begin{equation}\label{eq11}
              \tau_1 \equiv d^p\app \tau' \ \wedge \ p \le s \ \wedge\ \tau' \sqsubseteq \tau.
            \end{equation}
            Folosind \eqref{eq8}, \eqref{eq10} \c si regula {\scriptsize (T-LETREC)} avem c\u a
            \begin{equation}\label{eq12}
                \forall q. \Gamma \vdash (\text{letrec}_{d\app|\tau| \to |\sigma|}f := g) : [\iota \mapsto q] (d^{{\iota}}\app\tau \to \sigma)
            \end{equation}
            \c Tin\^ and cont de \eqref{eq10} alegem pe $q \equiv \iota$. Folosind lema de substitu\c tie \ref{subst_var}, \eqref{eq8} \c si \eqref{eq12} putem concluziona c\u a:
            \begin{equation}\label{eq13}
                \Gamma \vdash ([f \mapsto (\text{letrec}_{d|\tau| \to |\sigma|}f := g)]g) : [\iota \mapsto \hat {\iota}] (d^{\iota} \app \tau \to \sigma)
            \end{equation}
            Ra\c tion\^ and ca \^ in cazul {\scriptsize (T-CASE)} pentru $\Gamma \vdash t_2 = c\app [|\tau|] \app e : d^p \app\tau'$ ob\c tinem c\u a \done\todo{refacut argumentul}
            \begin{equation}\label{eq14}
                \exists r.  d^{\hat{r}} \tau \sqsubseteq d^p \app \tau'
            \end{equation}
            Conform cu lema \ref{sub_inversion} avem $p \ge \hat{r}$, deci exist\u a dou\u a posibilit\u a\c ti
            \begin{enumerate*}
                \item $p=j^n$ cu $n \ge 1$ . Conform lemei \done\todo{lema 3.8} \ref{stage_subst} putem aplica substitu\c tia $\iota \mapsto j^{n-1}$ relatiei \eqref{eq13} \c si \c tinand cont de \eqref{eq10} ob\c tinem
                \begin{equation}
                    \Gamma \vdash ([f \mapsto (\text{letrec}_{d|\tau| \to |\sigma|}f := g)]g) : d^{j^n} \app \tau \to [\iota \mapsto j^n] \sigma
                \end{equation}
                Cum din rela\c tiile \eqref{eq14} \c si \eqref{eq11} avem c\u a $\Gamma \vdash (c [|\tau|] e) : d^p\app \tau' \sqsubseteq d^p\app \tau$, folosind {\scriptsize (T-APP)} ob\c tinem:
                \begin{equation} \label{eq15}
                    \Gamma \vdash([f \mapsto (\text{letrec}_{d|\tau| \to |\sigma|}f := g)]g) \app (c [|\tau|] e) : [\iota \mapsto j^n] \sigma
                \end{equation}
                Dar din rela\c tia \eqref{eq10}, $\iota \text{ \emph{pos} } \sigma$, din \eqref{eq11} $j^n = p \le s$ \c si conform lemei \ref{stage_pos_subst} $[\iota \mapsto j^n] \sigma \sqsubseteq [\iota \mapsto s] \sigma$, deci conform \eqref{eq15} concluzion\u am c\u a
                \begin{equation}
                    \Gamma \vdash e_2 : [\iota \mapsto s] \sigma \equiv \tau_2
                \end{equation}
                \item $p = \infty^m $ cu $m \ge 0$. Folosind {\scriptsize (T-SUB)} deducem $\Gamma \vdash (c [|\tau|] e) : d^{\infty^{m+1}}\app \tau'$ \c si similar cu punctul precedent $\Gamma \vdash e_2 : [\iota \mapsto \infty^{m+1}]\sigma$. Avem $s \ge \infty^{m}$ deci
                \begin{equation}
                    \forall r.r \le \infty \Rightarrow \hat{\infty} \le \infty \Rightarrow \infty^{m+1} \le \infty^{m} \le s
                \end{equation}
                \^ In concluzie , $\Gamma \vdash e_2 : [\iota \mapsto s]\sigma\equiv \tau_2$. \qedhere
            \end{enumerate*}
        \end{enumerate*}
\end{description}
\end{proof}

\done\todo{de facut lemele sa arata ca lumea}
Vom prezenta \^ in continuare lemele folosite \^ in demonstra\c tie \citep{967408}. Majoritatea nu au fost invocate explicit, pentru a nu \^ incarca demonstra\c tia. Demonstra\c tiile implic\u a un procedeu de induc\c tie si constau \^ in manipul\u ari de ecua\c tii de rutin\u a.

\begin{lemma}\label{inversion}
Aceasta lem\u a furnizeaz\u a reciproce pentru regulile de deduc\c tie ale tipurilor.
\begin{enumerate}
\item $\Gamma \vdash x : \sigma \Rightarrow (x : \tau) \in \Gamma \textbf{ si } \tau \sqsubseteq \sigma$
\item $\Gamma \vdash e_1\app e_2 : \sigma \Rightarrow \Gamma \vdash e_1 : \tau_1 \to \tau_2 \textbf{ si }
                                                \Gamma \vdash e_2 : \tau_1 \textbf{ si }
                                                \tau_2 \sqsubseteq \sigma $
\item $\Gamma \vdash e \app[|\tau|] : \sigma  \Rightarrow \Gamma \vdash e : \Pi X . \tau_1 \textbf{ si }
                                                [X \mapsto \tau ] \tau_1 \sqsubseteq \sigma $
\item $\Gamma \vdash c : \sigma  \Rightarrow \exists s. \sigma \equiv \Pi X.\tau_1 \to \tau_2 \textbf{ si }
                                        \tau_1 \sqsubseteq [\iota \mapsto s]\theta_k \textbf{ si }
                                        d^{\hat{s}}\app X \sqsubseteq \tau_2$
\item $\Gamma \vdash \lambda x : {|\tau|}. e :\sigma \Rightarrow \sigma \equiv \tau_1 \to \tau_2  \textbf{ si }
                                                        \Gamma , x:\tau \vdash e : \tau_2' \textbf{ si }
                                                        \tau_1 \sqsubseteq \tau \textbf{ si }
                                                        \tau_2' \sqsubseteq \tau_2$
\item $\Gamma \vdash \text{\emph{case}}_{|\sigma|}\ e \text{ \emph{of} } \{ \vec{c} \Rightarrow \vec{e} \} : \sigma \Rightarrow
                        \Gamma \vdash e : d^{\hat{s}}\tau_1,
                        \Gamma \vdash e_k : [X \mapsto \tau_1, i \mapsto s] \theta_k \to \tau_2 \textbf{si }
                        \tau_2 \sqsubseteq \sigma$
\item $ \Gamma  \vdash (\text{\emph{letrec}}_{d |\tau| \to |\gamma|} f:=g) : \sigma \Rightarrow
        \Gamma,f : d^{{\iota}} \tau \to \gamma \vdash g : [\iota \mapsto \hat{\iota}] (d^{{\iota}}\app \tau \to \gamma) \textbf{ si }$
        $\qquad \iota \text{ \emph{pos} } \gamma \textbf{ si } \iota \notin \Gamma , \tau \textbf{ si } \exists s.[\iota \mapsto s] (d^{{\iota}} \tau \to \gamma) \sqsubseteq \sigma $
\end{enumerate}
\end{lemma}

\begin{lemma}\label{sub_inversion}
Lema de inversiune a reguli de subtip pentru tipuri de date.
$$ \theta \sqsubseteq d^s\app \tau \Rightarrow \theta \equiv d^r \app \sigma \textbf{ si } r \le s \textbf{ si } \sigma \sqsubseteq \tau $$
\end{lemma}

\begin{lemma}
Rela\c tia de subtip este invariant\u a la substitu\c tia de dimensinui.
$$ \tau_1 \sqsubseteq \tau_2 \Rightarrow [\iota \mapsto s]\tau_1 \sqsubseteq [\iota \mapsto s]\tau_2$$
\end{lemma}

\begin{lemma}\label{subst_sub}
Rela\c tia de subtip este invarianta la substitu\c tia de variabile de tip.
$$\tau \sqsubseteq \sigma \Rightarrow [X \mapsto \gamma]\tau \sqsubseteq [X \mapsto \gamma] \sigma $$
\end{lemma}

\begin{lemma}\label{subst_var}
Daca intr-o expresie $e$, o variabila liber\u a $x$ este \^ inlocuit\u a de o expresie de acela\c si tip $e'$, atunci tipul expresiei $e$ se conserv\u a.
$$\Gamma , x : \tau \vdash e : \sigma \wedge \Gamma \vdash e' : \tau \Rightarrow \Gamma \vdash [x \mapsto e']e : \sigma $$
\end{lemma}

\begin{lemma}\label{stage_inversion}
Monotonia func\c tiei $d^{\hat{x}} : s \to \overline{T}$.
$$ d^{\hat{r}} \tau \sqsubseteq d^{\hat{s}} \tau \Rightarrow r \le s$$
\end{lemma}

\begin{lemma} \label{stage_pos_subst}
Covarian\c ta tipurilor \^ in raport cu pozi\c tiile pozitive \c si contravarian\c ta \^ in raport cu cele negative.
\begin{gather*}
 \iota \text{ pos } \theta \wedge s \le r \Rightarrow [\iota \mapsto s] \theta \sqsubseteq [\iota \mapsto r] \theta \\
 \iota \text{ neg } \theta \wedge s \le r \Rightarrow [\iota \mapsto r] \theta \sqsubseteq [\iota \mapsto s] \theta
\end{gather*}
\end{lemma}

\begin{lemma}\label{stage_subst}
Polimorfismul variabilelor de dimensiune libere.
$$\Gamma \vdash e : \sigma \wedge  \iota \notin \Gamma \Rightarrow \forall s. \Gamma \vdash e : [\iota \mapsto s] \sigma$$
\end{lemma}

\begin{corollary}
System \fhat are proprietatea de siguranta.
\end{corollary}

\subsection{Adnot\u ari explicite}

\^ In cazul \^ in care termenii ar fi adnota\c ti explicit cu dimensiuni, proprietatea de conservare \c si deci cea de siguan\c ta nu ar mai avea loc.
\begin{example}[Barthe et al. \citep{DBLP:conf/tlca/BartheGP05}]
Consider\u am expresia
$$ pred = \text{\emph{letrec}}_{\textbf{\emph{Nat}}^{\iota}\to\textbf{\emph{Nat}}^{\iota}} f := \lambda x: \textbf{\emph{Nat}}^{\hat{\iota}}.\text{\emph{case}}_{\textbf{\emph{Nat}}^{\iota}}\ x \text{ \emph{of} } \{ z \Rightarrow z\ |\ s \Rightarrow \lambda z : \textbf{\emph{Nat}}^{\iota}.z \}$$
Conform regulii {\scriptsize (T-LETREC)} pentru orice dimensiune $s$, $pred : \textbf{\emph{Nat}}^s \to \textbf{\emph{Nat}}^s$, deci putem deduce c\u a ra\c tionamentul $y : \textbf{\emph{Nat}}^j \vdash pred \app (s \app y) : \textbf{\emph{Nat}}^j$ este valid. Totodat\u a, \^ in urma reducerii ob\c tinem $y : \textbf{\emph{Nat}}^j \nvdash (\lambda z : \textbf{\emph{Nat}}^i.z)\app y : \textbf{\emph{Nat}}^j$.
\end{example}

Absen\c ta adnot\u arilor cu dimensiuni exprim\u a o cuantificare universala a dimensiunilor peste toata expresia de tip. De exemplu, \^ in cazul func\c tiei $\lambda x : \textbf{Nat} . x$ putem afirma c\u a
$$\forall s . \emptyset \vdash (\lambda x : \textbf{Nat} . x) :  \textbf{Nat}^s \to  \textbf{Nat}^s \Leftrightarrow \emptyset \vdash (\lambda x : \textbf{Nat} . x) :  \forall s. \textbf{Nat}^s \to  \textbf{Nat}^s$$
Practic acest polimorfism la nivel de dimensiune ne spune c\u a func\c tia identitate definita pe numere naturale func\c tioneaza pe toate aproxim\u arile mul\c timii de numere naturale. Adnotarea cu dimensiuni ar defini o func\c tie identitate doar pe o anumit\u a aproximare.

\^ In cazul recursivit\u a\c tii textuale, func\c tia ob\c tinut\u a este prin natura sa definit\u a pe toate aproxim\u arile unui tip de date. E\c secul System \fhat de a avea proprietatea de conservare \^ in prezen\c ta adnot\u arilor cu dimensiuni se datoreaz\u a faptului c\u a o func\c tie lambda monomorifca este o subexpresie a unei defini\c tii textual recursive polimorfice.

\section{Normalizarea puternic\u a}

\^ In aceasta sec\c tiune vom demonstra propietatea de normalizare puternic\u a pentru orice expresie din Systm \fhat \^ in raport cu o rela\c tie de reducere mai generala dec\^ at cea folosit\u a la definirea semnaticii opera\c tionale a System \fhat. Demonstra\c tia prezentat\u a este extinderea demonstratiei din \citep{967408} pentru tipuri polimorfice dupa ideile prezentate \^ in \citep{1614481}.

\begin{theorem}
Secven\c ta de reduceri conform rela\c tiei $\to_{\beta\iota\mu}$ a unei expresii din System \fhat este finita. Unde $e_1 \to_{\beta\iota\mu} e_2$ dac\u a $e_1$ se reduce la $e_2$ prin aplicarea regulilor de reducere {\scriptsize (E-APP),(E-TAPP),(E-CASE)} \c si {\scriptsize (E-LETREC)} pentru orice subexresie (nu doar \^ in cele determinate de regulile {\scriptsize (CTX-APP),(CTX-TAPP),(CTX-CASE)} \c si {\scriptsize  (CTX-LETREC)}).
\end{theorem}

Formal, mul\c timea expresiilor cu proprietatea de normalizare puternic\u a (strongly-normalizing sau $\in \textbf{SN}$) este definit\u a ca cea mai mic\u a mul\c time cu urm\ atoarea proprietate:
\begin{equation}
    \forall e . \quad (\forall e'. \quad e \to_{\beta\iota\mu} e' \Rightarrow e' \in {\textbf{SN}} ) \Rightarrow  e \in {\textbf{SN}}
\end{equation}
Vom spune c\u a orice expresie $e \in {\bf SN}$ este \emph{reductibil\u a}.

Vom \^ incerca s\u a asociem fiecarui tip al System \fhat o mul\c time (\emph{mul\c time saturata} \citep{967408}) de expresii reductibile care au acel tip. Apoi vom demonstra c\u a orice termen apartin\^ and acelui tip face parte din mul\c timea asociata. Acest lucru furnizeaz\u a demonstra\c tia teoremei de normalizare puternic\u a.

\subsection{Mul\c timi saturate}

Pentru \^ inceput vom introduce ni\c ste defini\c tii:
\begin{definition}
Un {\bf context slab} reprezint\u a o loca\c tie intr-o expresie din System \fhat unde ar putea fi f\u acuta o reducere dupa regulile {\scriptsize (CTX-APP),(CTX-TAPP),(CTX-CASE)} si {\scriptsize  (CTX-LETREC)}. Contextele slabe sunt generate de gramatica:
\begin{center}
E[] :=  []   $\:|\:$   E[] e   $\:|\:$   E[] [$|\tau|$]   $\:|\:$   $\text{\emph case}_\tau$ E[] of \{ $\vec{c} \Rightarrow \vec{e}$ \}
\end{center}
Un context se nume\c ste {\bf context slab de baz\u a} dac\u a toate subexpresiile contextului sunt reductibile.
\end{definition}

\begin{definition}
O expresie se nume\c ste \textbf{expresie de baz\u a} dac\u a este de forma E[x] unde E este un context slab de ba\u za, \c si x este o variabil\u a. Mul\c timea expresiilor de baz\u a se noteaz\u a cu \textbf{B}.
\end{definition}

Se poate demonstra prin induc\c tie dup\u a structura contextului, urmatoarea lem\u a:
\begin{lemma}
Orice expresie de baz\u a este reductibil\u a.
\end{lemma}

\begin{definition}
Rela\c tia de \textbf{reducere slab\u a} este rela\c tia de reducere \^ in care regulile {\scriptsize (E-APP),(E-TAPP),(E-CASE)} \c si {\scriptsize (E-LETREC)} se aplic\u a doar pentru subexpresii ce corespund unui context slab. Ea se noteaz\u a cu $\to_k$.
\end{definition}

\begin{definition}
O mul\c time de expresii $X$ System \fhat se nume\c ste \textbf{mul\c time saturat\u a} dac\u a:
\begin{enumerate*}
\item Orice expresie din $X$ este reductibil\u a.
\item Orice expresie de baz\u a face parte din $X$.
\item Daca o expresie $e$ este reductibil\u a \c si $e \to_k e' \in X$ atunci $e \in X$.
\end{enumerate*}
Mul\c timea tuturor multimilor saturate va fi notat\u a cu \textbf{SAT}. Pentru orice mul\c time $X$ de expresii, se noteaz\u a cu $\overline{X} = \{ e \in SN \ |\ \exists e' \in Base \cup X. \quad e \to_k^* e'\}$ \^ inchiderea multimii $X$.
\end{definition}

Pentru fiecare tip din System \fhat va fi construit\u a inductiv o mul\c time saturat\u a. Astfel va trebui s\u a folosim unele propriet\u a\c ti de inchidere a mul\c timii \emph{SAT} relative la operatorii folosi\c ti \^ in acest proces de construc\c tie.

\begin{lemma}
\begin{enumerate*}
\item Pentru orice mul\c time de expresii $X \in SN$ avem $\overline{X} = \bigcap_{Y \supset X, Y \in SAT}Y $.
\item \^ Inchiderea unei mul\c timi este saturat\u a : $\overline{X} \in SAT$.
\item \^ Inchiderea comut\u a cu reuniunea $\overline{X_1 \cup \dots \cup X_n} = \overline{X_1} \cup \dots \cup \overline{X_n}$.
\item Dac\u a $X_i$ sunt mul\c timi saturate pentru orice $i \in I$ atunci $\bigcup_{i \in I} X_i$ este mul\c time saturat\u a.
\end{enumerate*}
\end{lemma}

\done\todo{NU ESTE}
\begin{lemma}
Dac\u a $X,Y$ sunt mul\c timi saturate, atunci $X \to Y = \{ e \: |\: \forall e' \in X.\quad e\app e' \in Y \} $ este mul\c time saturat\u a.
\end{lemma}
\begin{comment}
\begin{proof}[Demonstratie]
Se observa ca orice expresie $e \in X \to Y$ este reductibil\u a:
\begin{equation}
\forall e'.\quad e\app e' \in Y \Rightarrow e\app e' \in SN \Rightarrow e \in SN
\end{equation}
In continuare vom demonstra ca $B \subset X \to Y$. Fie $e \in B$ si $e' \in X $. Din faptul ca $e' \in X \subset SN$, rezulta ca $[]\app e'$ este un context slab, deci $e\app e' \in B \subset Y$. Deci $e \in X \to Y$.

Fie $e \in SN$ cu $e \to_k e'$ si $e' \in X \to Y$. Consideram o expresie $t \in X \subset SN$ arbitrara . Cum contextul $ []\app t $ este context slab, avem ca $e\app t \to_k e'\app t$. Cum $t\in SN$ avem $e'\app t \in Y \subset SN$. Din lema urmatoare \todo{e t in SN} rezulta ca $e \app t \in SN$ si cum $e \app t \to_k e' \app t \in Y$ inseamna ca $Y$ indeplineste si cea de-a treia conditie pentru multimi saturate.
\end{proof}
\end{comment}

\begin{lemma}
Fie $t \in SAT$ un tip System \fhat, atunci mul\c timea $\{ e \: |\: \forall \sigma \in T .\quad e\app \sigma \in t\}$ este mul\c time saturat\u a.
\end{lemma}

\subsection{Interpretarea limbajului}

Vom construi \^ int\^ ai o interpretare pentru dimensiuni, asociind fiecarei dimensiuni un ordinal num\u arabil.

\begin{definition}
Mul\c timea de ordinali num\u arabili $Ord$ este cea mai mica mul\c time nenumar\u abila cu o rela\c tie de ordine totala \fixme{well-founded} pentru care $I_x := \{ y \: |\: y < x \}$ este num\u arabila pentru orice $x$.
\end{definition}

\begin{remark}
Mul\c timea ordinalilor este izomorfa cu "mul\c timea" \^ in care fiecare element este chiar mul\c timea elementelor mai mici decat el. Aceasta mul\c time este total ordonat\u a, iar totalitatea elementelor care reprezint\u a mul\c timi num\u arabile formeaz\u a mul\c timea ordinalilor num\u arabili. Not\u am cu $\Omega$ primul ordinal nenum\u arabil
\end{remark}

Plec\^ and de la o func\c tie care asociaz\u a cate un ordinal num\u arabil fiecarei variabie de dimensiune $v_s : S \to Ord$ definim o interpretare a dimensiunilor astfel:
\begin{align*}
&\langle x \rangle_{v_s} = v_s(x) \\
&\langle \hat{s} \rangle_{v_s} =  succ(\langle s \rangle_{v_s} ) = \inf \{ I_{\langle s \rangle_{v_s} } \cup \{\langle s\rangle_{v_s} \} \} \\
&\langle \hat{\infty} \rangle_{v_s} = \langle \infty \rangle_{v_s} = \Omega
\end{align*}

Plec\^ and de la o interpretare a variabilelor de dimensiune $v_s : S \to Ord$, \c si de la o interpretare a variabilelor de tip $v_T : T \to SAT$ se poate definim interpretarea tipurilor astfel:
\begin{align*}
&\langle X \rangle_{v_s,v_T} = v_T(X) \\
&\langle \tau \to \sigma \rangle_{v_s,v_T} =  \langle \tau \rangle_{v_s,v_T} \to \langle \sigma \rangle_{v_s,v_T} \\
&\langle \Pi X. \tau \rangle_{v_s,v_T} = \{ e \: |\: \forall \sigma \in T .\quad e\app \sigma \in \langle \tau \rangle_{v_s,[X\mapsto \langle \sigma \rangle_{v_s,v_T} ]v_T}\} \\
&\langle d^{s}\app\tau \rangle_{v_s,v_T} = D_d( \tau , \langle s \rangle_{v_s}) = D_d^{def} ( \tau, \langle \tau \rangle_{v_s,v_T}, \langle s \rangle_{v_s})
\end{align*}
unde $D_d(X,s)$ este definita prin induc\c tie transfinit\u a astfel:
\begin{align*}
& D_d^{def}( \tau, S , 0) = \overline{\emptyset} \\
& D_d^{def}( \tau, S, succ(x)) = \overline{\bigcup \{c \app \tau\app e \: | \: e \in \langle \theta \rangle_{[ \iota \mapsto x]v_s,[X \mapsto S] v_T}, c : \theta\to d^{\hat{\iota}} \app X \}} \\
& D_d^{def}( \tau, S, \lambda) = \bigcup\{D_d^{def}(\tau, X,s) \: | \: s < \lambda \} \text{ daca $\lambda$ nu are predecesor }
\end{align*}

\begin{remark}
Definirea printr-o recuren\c t\u a transfinit\u a a fost posibil\u a datorit\u a faptului c\u a rela\c tia de ordine \^ intre ordinali este \fixme{well-founded}. Datorit\u a faptului c\u a \^ in defini\c tia $D_d^{def}( \tau, S, succ(x))$ apare interpretarea lui $\theta$ care la randul s\u au poate con\c tine pe $d$ sau alte tipuri de date $d'$, defini\c tia poate p\u area circular\u a. Totu\c si, faptul c\u a un constructor creeaz\u a o valoare cu dimensiune mai mare dec\^ at argumentul s\u au ne asigur\u a c\u a sunt folosite interpret\u ari ale lui $d$ doar pentru dimensiuni pentru care au fost deja calculate.
\end{remark}
\begin{remark}
Av\^ and \^ in vedere c\u a un tip recursiv $d$ poate avea constructori cu argumente de tip $d'$ doar dac\u a $d'$ apare \^ in program \^ inainte de de $d$ \c si faptul c\u a interpretarea se face \^ in ordinea declara\c tiilor din program, ne asigur\u a ca defini\c tia recursiva pentru interpret\u ari nu este circular\u a.
\end{remark}
\begin{remark}
Atunci c\^ and un ordinal nu are predecesor, el este numit ordinal limit\u a pentru c\u a poate fi v\u azut ca $x = \lim_{y < x} y $. Un exemplu de acest gen este $\infty = \sup_{n \in \mathbb{N}}n$.
\end{remark}
\done\todo{de ce sunt doar aceste cazuri?}

Urm\u atoarea propozi\c tie asigur\u a corectitudinea interpret\u arii dimensiunilor \^ in ceea ce prive\c ste rela\c tia de ordine.
\begin{proposition}
\begin{align*}
s \le \widehat{s}           \: &\equiv \: D_d(S,x) \subseteq D_d(S,succ(x))\\
\widehat{\infty} \le \infty \: &\equiv \: D_d(S,\Omega) = D_d(S, \Omega+1)
\end{align*}
\end{proposition}
\begin{proof}[Demonstra\c tie]
Faptul c\u a se ajunge la un punct fix pentru un ordinal mai mic dec\^ at $\Omega$ se da\-to\-re\-a\-z\u a faptului c\u a la fiecare pas, mu\-l\c ti\-me\-a $D_d(S,x)$ cre\c ste dar fiind mul\c time de expresii System \fhat este numarabil\u a, \^ in timp ce $\Omega$ nu este num\u arabil.
\end{proof}
Analog se poate defini \c si o interpretare a expresiilor prin alte expresii System \fhat pornind de la o interpretare a variabiellor libere.

\subsection{Corectitudinea interpret\u arii}
\begin{definition}
Fie o interpretare dat\u a de tripletul $(\pi,\zeta, \rho)$ - interpret\u ari ale variabilelor libere de dimensiune, tip \c si termeni. Aceast\u a interpretare satisface un context de tip dac\u a $\rho(e) \in \langle \tau \rangle_{\pi,\zeta}$ pentru orice $(x:\tau) \in \Gamma$ \c si se noteaz\u a cu $(\pi,\zeta, \rho) \models \Gamma$. Ea satisface o deduc\c tie $\Gamma \vdash e : \tau$ dac\u a
    $$(\pi,\zeta, \rho) \models \Gamma \Rightarrow \langle e \rangle \in \langle \tau \rangle_{\pi,\zeta}$$
Dac\u a o deduc\c tie este satisf\u acuta\u  de orice interpretare atunci ea se nume\c ste valid\u a \c si vom scrie $\Gamma \models e : \sigma$
\end{definition}

Vom demonstra prin induc\c tie urmatoarea propozi\c tie, proprietatea de normalizare puternica fiind un caz particular al acestei propozi\c tii.
\begin{proposition}\label{soundness}
$$ \Gamma \vdash e : \sigma \Rightarrow   \Gamma \models e : \sigma$$
\end{proposition}
\begin{proof}[Demonstra\c tie]
Se demonstreaz\u a prin inductie structural\u a pe arborele de deduc\c tie al propozi\c tiei $\Gamma \vdash e : \sigma$. Cazurile specifice, care nu apar \^ in alte demonstra\c tii de normalizare puternic\c a, ca de exemplu pentru System F,  sunt pentru care ultima regula aplicata este {\scriptsize (T-CONS), (T-CASE), (T-LETREC), (T-TABS)} sau {\scriptsize (T-TAPP)}. Cazutile corespunz\u atoare regulilor {\scriptsize (T-TAPP)} \c si {\scriptsize (T-TABS)} sunt triviale.
\begin{description}
  \item[{\scriptsize (T-CONS)}] Trebuie s\u a ar\u at\u am c\u a $c = \langle c \rangle_{\rho} \in \langle \Pi X. \theta \to d^{\hat{\iota}}\app X \rangle_{\pi,\zeta} $, deci conform defini\c tiei, c\u a
      \begin{equation}
      \forall \tau. \quad c\app \tau \in \langle [X \mapsto \tau] \theta \rangle_{\pi,\zeta} \to \langle d^{\hat{\iota}} \tau \rangle_{\pi,\zeta}
      \end{equation}
      care este echivalenta cu
      \begin{equation}
      \forall \tau, e \in \langle [X \mapsto \tau] \theta \rangle_{\pi,\zeta} . \quad c\app \tau\app e \in \langle d^{\hat{\iota}} \tau \rangle_{\pi,\zeta}
      \end{equation}
      Lucru adevarat din defini\c tia lui $\langle d^{\hat{\iota}} \tau \rangle_{\pi,\zeta} = \bigcup \{ c\app \tau\app e \:|\: e \in \langle \theta \rangle_{[\iota \to \langle \iota \rangle_{\pi}]\pi, [ X \mapsto \langle \tau \rangle_{\zeta}]\zeta} \} $

  \item[{\scriptsize (T-CASE)}] Trebuie s\u a ar\u at\u am c\u a $\langle \text{case}_{\sigma}\ e \text{ of } \{ \vec{c} \Rightarrow \vec{e} \} \rangle_{\rho} \in \langle \sigma \rangle_{\pi,\zeta} $ \^ in condi\c tiile \^ in care, din ipoteza de induc\c tie avem $\langle e \rangle_{\rho} \in \langle d^{\hat{s}}\tau \rangle_{\pi,\zeta}$ si $\langle e_k \rangle_{\rho} \in \langle [X\mapsto \tau, i\mapsto s] \theta_k \rangle_{\pi,\zeta} \to \langle \sigma \rangle_{\pi,\zeta}$.

  \c Stim c\u a $\langle e \rangle_{\rho} \in \langle d^{\hat{s}}\tau \rangle_{\pi,\zeta}$ \c si din defini\c tia \^ inchiderii trebuie s\u a $\exists e'$ astfel \^ incat $\langle e \rangle_{\rho}\to_k^* e'$ si
  \begin{equation}
  e' \in B \cup \bigcup \{c_k \app \tau\app t \: | \: t \in \langle \theta_k \rangle_{[ \iota \mapsto s]\pi,[X \mapsto \langle \tau \rangle_{\pi, \zeta } ] \zeta}\}
  \end{equation}

  Demonstr\u am acum c\u a $\langle \text{case}_{\sigma}\ e' \text{ of } \{ \vec{c} \Rightarrow \vec{e} \} \rangle_{\rho} \in \langle \sigma \rangle_{\pi,\zeta}$ prin tratarea a dou\u a cazuri
  \begin{enumerate*}
    \item $ e' \in B$. \^ In acest caz
        \begin{equation}
            \text{case}_{\sigma}\ \langle e \rangle_{\rho}\text{ of } \{ \vec{c} \Rightarrow \vec{\langle e\rangle_{\rho}} \} \to_k^*
            \text{case}_{\sigma}\  e' \text{ of } \{ \vec{c} \Rightarrow \vec{\langle e\rangle_{\rho}} \}
            \in B \subseteq \langle \sigma \rangle_{\pi,\zeta}
         \end{equation}
         Deci concluzia este demonstrat\u a av\^ and \^ in vedere c\u a $\langle \sigma \rangle_{\pi,\zeta} $ este \^ inchisa la expansiune slaba (opusul reducerii slabe).
    \item $ e' = c_k \app \tau \app t $ cu $t \in \langle \theta_k \rangle_{[ \iota \mapsto \langle s \rangle_{\pi}]\pi,[X \mapsto \langle \tau \rangle_{\pi, \zeta } ] \zeta} = \langle [X\mapsto \tau, i\mapsto s] \theta_k \rangle_{\pi,\zeta}$. In acest caz ob\c tinem
        \begin{equation}
            \text{case}_{\sigma}\ e' \text{ of } \{ \vec{c} \Rightarrow \vec{\langle e\rangle_{\rho}} \} \to_k
            \langle e_k  \rangle_{\rho}\app t \in  \langle \sigma \rangle_{\pi,\zeta}
        \end{equation}

        Cum $\text{case}_{\sigma}\ e' \text{ of } \{ \vec{c} \Rightarrow \vec{\langle e\rangle_{\rho}} \}$ este reductibil\u a \^ inseamna c\u a $\in  \langle \sigma \rangle_{\pi,\zeta}$. Analog, expresia $\text{case}_{\sigma}\ \langle e \rangle_{\rho} \text{ of } \{ \vec{c} \Rightarrow \vec{\langle e\rangle_{\rho}} \}$ este reductibil\u a (lema \ref{cond_reductibil}) \c si se reduce la un termen din $\langle \sigma \rangle_{\pi,\zeta}$, deci apar\c tine acestei mul\c timi.
  \end{enumerate*}

  \item[{\scriptsize (T-LETREC)}] \^ In acest ultim caz trebuie sa ar\u at\u am c\u a
    \begin{equation} \label{concl}
        \langle \text{letrec}_{d|\tau| \to |\theta|}f := g \rangle_{\rho} \in
        \langle d^s\app \tau \to [\iota \mapsto s] \theta \rangle_{\pi,\zeta} =
        \langle d^s\app \tau  \rangle_{\pi,\zeta}  \to \langle \theta  \rangle_{[\iota \mapsto \langle s \rangle_{\pi}] \pi,\zeta}
    \end{equation}
    Not\u am cu $\pi_0 = [\iota \mapsto \langle s \rangle_{\pi}]\pi$ si $\rho_0 = [f \mapsto f]\rho$. Atunci obiectivul nostru devine
    \begin{equation*}\label{concl_reduced}
        (\text{letrec}_{d|\tau| \to |\theta|} f := \langle g \rangle_{\rho_0}) \app e \in \langle \theta \rangle_{\pi_0,\zeta}
        \text{  pentru  } \forall e \in \langle d^\iota\app \tau \rangle_{\pi_0,\zeta}
    \end{equation*}
    Deoarece $f$ este variabila libera \^ in corpul func\c tiei textual recursive $g$, are loc rela\c tia $\langle f \rangle_{\rho_0} = \rho_0(f) = f \in B \subseteq \langle d^\iota\app\tau\to\theta \rangle_{\pi,\zeta}$. \^ In consecin\c ta, conform ipotezei de induc\c tie, avem c\u a $\langle g \rangle_{\rho_0} \in \langle d^{\hat{\iota}}\app\tau\to [\iota \mapsto \hat{\iota}]\theta \rangle_{\pi,\zeta} \subseteq SN$.

    Vom demonstra \eqref{concl_reduced} prin induc\c tie trasnfinit\u a dup\u a ordinalul $\pi_0(\iota)$
    \begin{equation}
        \forall \pi_0,\zeta,\rho_0,e \in \langle d^\iota\app \tau \rangle_{\pi_0,\zeta}.\:  (\text{letrec}_{d|\tau| \to |\theta|} f := \langle g \rangle_{\rho_0}) \app e \in \langle \theta \rangle_{\pi_0,\zeta}
    \end{equation}
    \begin{description*}
    \item [Caz 1: $\pi_0(\iota)=0$] Fie $e \in \langle d^{\iota} \tau \rangle_{\pi_0,\zeta} = \overline{\emptyset}$. Atunci $\exists e'$ astfel \^ inc\^ at $e \to_k^* e'$ si $e' \in B$. Deci
        \begin{equation}
            (\text{letrec}_{d|\tau| \to |\theta|} f := \langle g \rangle_{\rho_0}) \app e \to_k^* (\text{letrec}_{d|\tau| \to |\theta|} f := \langle g \rangle_{\rho_0}) \app e' \in B
        \end{equation}
        Cum $(\text{letrec}_{d|\tau| \to |\theta|} f := \langle g \rangle_{\rho_0}) \app e$ este reductibil\u a (lema \ref{cond_reductibil}) \c si se reduce la o expresie de baz\u a \^ inseamna c\u a face parte din orice mul\c time saturat\u a deci \c si din $\langle d^\iota\app \tau \rangle_{\pi_0,\zeta}$

    \item [Caz 2: $\pi_0(\iota)=succ(y)$] Fie $\pi' = [\iota \mapsto y]\pi $ si $\rho' = [f \mapsto (\text{letrec}_{d|\tau| \to |\theta|} f := \langle g \rangle_{\rho_0})] \rho$. Din ipoteza de induc\c tie interioar\u a avem c\u a
        \begin{equation}
            \langle f \rangle_{\rho'} = (\text{letrec}_{d|\tau| \to |\theta|} f := \langle g \rangle_{\rho_0}) \in \langle d^{\iota}\app \tau \to \theta \rangle_{\pi',\zeta}
        \end{equation}
        Iar din ipoteza de induc\c tie exterioar\u a, avem \^ in continuare
        \begin{equation}\label{eq16}
        \langle g \rangle_{\rho'} \in \langle d^{\hat{\iota}}\app \tau \to [\iota \mapsto \hat{\iota}]\theta \rangle_{\pi',\zeta} =
        \langle d^{{\iota}}\app \tau \to \theta \rangle_{\pi_0,\zeta}
        \end{equation}
        Cum $e \in \langle d^{\iota} \tau \rangle_{\pi_0,\zeta}$, conform defini\c tiei se reduce la $e'$ care este expresie de baz\u a, caz \^ in care demonstra\c tia este similar\u a cu cea de la cazul anterior, sau are forma $e' = c\app \tau\app t , t \in \langle d^\iota\app \tau \rangle_{\pi_0,\zeta}$. Atunci, conform \eqref{eq16}, avem
        $$
        (\text{letrec}\ f := \langle g \rangle_{\rho_0})\app e' \to_k ([f \mapsto (\text{letrec}\ f := \langle g \rangle_{\rho_0})] \langle g \rangle_{\rho_0}) \app e' = \langle g \rangle_{\rho'}\app e' \in \langle \theta \rangle_{\pi_0,\zeta}
        $$
        Cum expresia $(\text{letrec}\ f := \langle g \rangle_{\rho_0})\app e'$ este reductibil\u a, \^ inseamna c\u a ea face parte din mul\c timea saturat\u a $\langle \theta \rangle_{\pi_0,\zeta}$. Similar, $(\text{letrec}\ f := \langle g \rangle_{\rho_0})\app e$ este reductibil\u a (lema \ref{cond_reductibil}) \c si se reduce la un element din $\langle \theta \rangle_{\pi_0,\zeta}$, deci apar\c tine ea insa\c si lui $\langle \theta \rangle_{\pi_0,\zeta}$.
    \item [Caz 3: $\pi_0(\iota)=\sup_{y<x}y$] \^ In acest caz avem $e \in \langle d^{\iota} \tau \rangle_{\pi_0,\zeta} = \bigcup _{y < x}\langle d^{\iota} \tau \rangle_{[\iota \mapsto y]\pi_0,\zeta}$ deci $e$ apar\c tine unuia din termenii reuniunii, fie el $\langle d^{\iota} \tau \rangle_{[\iota \mapsto y]\pi_0,\zeta}$. Din ipoteza de induc\c tie:
         $$
            (\text{letrec}_{d|\tau| \to |\theta|} f := \langle g \rangle_{\rho_0}) \app e \in \langle \theta \rangle_{[\iota \mapsto y]\pi_0,\zeta}
         $$
        Dar $\iota \text{ pos } \theta$, \c si concluzia este demonstrat\u a pentru c\u a $\langle \theta \rangle_{[\iota \mapsto y]\pi_0,\zeta} \subset \langle \theta \rangle_{\pi_0,\zeta}$. \qedhere
    \end{description*}
\end{description}
\end{proof}

\begin{lemma}\label{cond_reductibil}
\^ In cursul demonstra\c tiei am folosit urmato\u arele condi\c tii suficiente pentru nor\-ma\-li\-za\-re\-a unei expresii:
\begin{enumerate*}
\item Dac\u a $e \in SN$ \c si $e \to_k e'$ \c si $\text{\emph{case}}_{\sigma}\ e' \text{ \emph{of} } \{ \vec{c} \Rightarrow \vec{e} \}  \in SN$, atunci $\text{\emph{case}}_{\sigma}\ e \text{ \emph{of} } \{ \vec{c} \Rightarrow \vec{e} \} \in SN$.

\item Dac\u a $e \in SN$ \c si $e \to_k e'$ \c si $(\text{\emph{letrec}}_{\dots} f :=  g)\app e' \in SN$, atunci $(\text{\emph{letrec}}_{\dots} f :=  g)\app e \in SN$.

\item Dac\u a $t,g, [f \mapsto(\text{\emph{letrec}}_{\dots} f :=  g)] g\app (c\app \tau\app t) \in SN$, atunci $(\text{\emph{letrec}}_{\dots} f :=  g) \app (c\app \tau\app t) \in SN$
\end{enumerate*}
\end{lemma}

\begin{remark}
Urm\u atorul exemplu ilustreaz\u a de ce nu a fost suficient s\u a interpret\u am dimensiunile \^ in numere naturale. Intuitiv, vom codifica ordinalii num\u arabili \^ in System \fhat prin urmatorul tip de date
$$ Datatype \ \textbf{Ord} := oz : \textbf{Ord}^{\hat{\iota}} \:|\: os : \textbf{Ord}^{{\iota}} \to \textbf{Ord}^{\hat{\iota}} \:|\: olim : (\textbf{Nat} \to \textbf{Ord}^{{\iota}}) \to \textbf{Ord}^{\hat{\iota}}$$
\^ In cazul interpret\u arii acestui tip, procedeul iterativ de interpretare pentru tipuri recursive se aplic\u a \^ in mod netrivial pentru fiecare ordinal.
\end{remark}

\begin{remark}
Dup\u a cum se poate observa, nu orice element din interpretarea unui tip corespunde unei expresii cu acel tip. Intuitiv, elementele ap\u arute \^ in plus provin de la aproximarea de dimensiune 0 a tipului, adic\u a elemente construite cu zero constructori.
\end{remark}

\begin{corollary}
System \fhat are proprietatea de normalizare puternic\u a.
\end{corollary}
\begin{proof}[Demonstra\c tie]
Fie $e$ o expresie \^ in System \fhat pentru care $\Gamma \vdash e : \sigma$. Atunci deduc\c tia $\Gamma \vdash e : \sigma$ este satisfacut\u a de orice interpretare, deci \c si de interpretarea care duce variabilele libere din $e$ \^ in ele \^ insele. \^ In consecint\u a avem c\u a $e \in \langle \sigma \rangle \in SAT$, deci expresia $e$ este membr\u a a unei mul\c timi saturate \c si \^ in consecin\c ta reductibil\u a.
\end{proof}

\subsection{Confluen\c ta}
O alt\u a proprietate str\^ ans legat\u a  de cea de normalizare, care atesta existen\c ta unei forme normale pentru fiecare termen, este cea de confluen\c ta care atest\u a unicitatea.

\begin{corollary}
Rela\c tia de reducere pentru System \fhat este confluenta.
\end{corollary}
\begin{proof}[Demonstra\c tie]
Deoarece \^ in procedeul de reducere \^ in care se folosesc ca reguli de context {\scriptsize (CTX-APP),(CTX-TAPP), (CTX-CASE)} la fiecare pas exista maxim o regul\u a care poate fi aplicat\u a,  exista cel mult o form\u a normal\u a la care se poate ajunge.
\end{proof}

\section{Tipuri principale}
\label{tip_princ}
\done\todo{SysF star si de ce are asta tipuri principale}
Asa cum este el definit, System \fhat nu are tipuri principale, adic\u a unele expresii nu au un cel mai general tip \^ in sensul rela\c tiei de subtip.
\begin{example}[Barthe et al. \citep{DBLP:conf/tlca/BartheGP05}]
Un exemplu de expresie care nu are un cel mai general tip este urmatoarea:
$$square := \lambda f : \textbf{Nat} \to \textbf{Nat}. \lambda x : \textbf{Nat}. f \app f\app x$$
Pentru $square$ pot fi asociate tipurile $(\textbf{Nat}^\iota \to \textbf{Nat}^\iota) \to \textbf{Nat}^\iota \to \textbf{Nat}^\iota$ \c si $(\textbf{Nat}^\iota \to \textbf{Nat}^\infty) \to \textbf{Nat}^\iota \to \textbf{Nat}^\infty$. Pentru aceste tipuri nu exist\u a un supertip comun.
\end{example}

Din aceasta cauz\u a s-au introdus tipurile cu pozi\c tie \citep{1614481}, care adnoteaz\u a o parte dintre constructori de tip cu $\star$ \^ in declara\c tiile de tip LETREC. \c Tin\^ and cont de aceste adnot\u ari regula {\scriptsize (T-LETREC)} se schimb\u a astfel

\begin{prooftree}
\AxiomC{$\overline{\Gamma}, f : d^\iota\tau \to \overline{\theta} \vdash e : d^{\hat{\iota}}\tau \to [\iota \mapsto \hat{\iota}] \overline{ \theta}$}
\AxiomC{$\iota \text{ pos } \overline{\theta} $}
\AxiomC{$d^\iota\tau \to \overline{\theta} \approx_{\iota} d^\star|\overline{\tau}| \to |\overline{\theta}|^\star$}

\RightLabel{\scriptsize (T-LETREC$\star$)}
\TrinaryInfC{$\overline{\Gamma} \vdash (\text{letrec}_{d^\star|\overline{\tau}| \to |\overline{\theta}|^\star} f = e) : d^s \overline{\tau} \to [\iota \mapsto s]\overline{\theta}$}
\end{prooftree}

unde $\tau_1 \approx_{\iota} \tau_2$ dac\u a $\tau_1$ si $\tau_2$ au aceea\c si structur\u a \c si un constructor este adnotat cu $\widehat{ \iota }$ (al $k$-lea succesor) \^ in $\tau_1$ dac\u a \c si numai dac\u a este adnotat cu $\star$ in $\tau_2$. Cu ajutorul acestei adnot\u ari se poate sepcifica mai exact tipul dorit al unei expresii. \^ In sec\c tiunea dedicata algoritmului de verificare a tipului se poate vedea ca acesta \^ intoarce o clasa de tipuri, ci nu un singur tip - cel mai general.

